(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Tuples:
G(a) → c(G(b), B)
B → c1(F(a, a))
F(a, a) → c2(G(d))
S tuples:
G(a) → c(G(b), B)
B → c1(F(a, a))
F(a, a) → c2(G(d))
K tuples:none
Defined Rule Symbols:
g, b, f
Defined Pair Symbols:
G, B, F
Compound Symbols:
c, c1, c2
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
F(a, a) → c2(G(d))
B → c1(F(a, a))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Tuples:
G(a) → c(G(b), B)
S tuples:
G(a) → c(G(b), B)
K tuples:none
Defined Rule Symbols:
g, b, f
Defined Pair Symbols:
G
Compound Symbols:
c
(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
G(a) → c(G(b), B)
We considered the (Usable) Rules:
b → f(a, a)
f(a, a) → g(d)
And the Tuples:
G(a) → c(G(b), B)
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(B) = 0
POL(G(x1)) = x1
POL(a) = [1]
POL(b) = 0
POL(c(x1, x2)) = x1 + x2
POL(d) = 0
POL(f(x1, x2)) = 0
POL(g(x1)) = 0
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Tuples:
G(a) → c(G(b), B)
S tuples:none
K tuples:
G(a) → c(G(b), B)
Defined Rule Symbols:
g, b, f
Defined Pair Symbols:
G
Compound Symbols:
c
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))